T:Type, eq:EqDecider(T), d1, d2:a:T fp Type.
non-void(d1)  non-void(d2)  non-void(d1  d2) 

latex

Definitions	t  T, P  Q, x:A. B(x), x,y. t(x;y), EqDecider(T), x. t(x), a:A fp B(a), Top, x  dom(f), b, , xdom(f). v=f(x)   P(x;v), f  g, non-void(d)
Lemmas	fpf-all wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, deq wf, fpf-all-join-decl